\chapter{minisat}
\section{Introduction}
Minisat est un logiciel de r\'esolution de probl\`emes SAT open source.
Cette partie du devoir est constitu\'ee de 3 algorithmes :
1. Transformation d'une instance du probl\`eme VC en une instance du
probl\`eme SAT.
2. Utilisation de minisat pour une r\'esolution de l'instance de SAT.
3. Transformation d'une solution fournie par minisat en couverture de
l'instance initiale de VC.
L'implementation de la partie minisat du programme découle des
algorithmes décrits dans chaque sous-section Algorithme. 

\section{Algorithme de transformation VC -> SAT}
\subsection{Algorithme}
Soit G = (V,E) le graphe du probl\`eme VC et S le probl\`eme sous forme SAT. \\
S est une liste donc $S\gets(v,u)$ signifie que l'on ajoute le couple (a,b) \`a S.
\begin{algorithmic}
\FORALL{$v \in V$}
\FORALL{$u \in Adj(v)$}
\STATE $S \gets (v,u)$
\ENDFOR
\ENDFOR
\end{algorithmic}
\subsection{Commentaires}
Cet algorithme enregistre dans S tous les couples (u,v) de sommets reli\'es par
une ar\^ete. La complexité est de O(m) o\`u m = |E| car on evalue deux fois
chaque ar\^ete, lorsque l'on ajoute les paires (u,v) et (v,u).
Chaque paire représente une disjonction du probl\`eme SAT.

\section{Utilisation de minisat}
\subsection{Algorithme}
1. Conversion du probl\`eme VC en probl\`eme SAT
2. Ecriture du probl\`eme SAT dans un fichier
3. Execution de minisat sur le fichier
4. Lecture de la solution produite par minisat
5. Conversion de la solution en couverture du probl\`eme VC
\subsection{Commentaires}
Pour l'\'ecriture du probl\`eme SAT, on transforme chaque paire (u,v) du
probleme en une ligne dans le fichier : ``u v 0''.
On \'ecrit au d\'ebut du fichier la ligne : ``p cnf X Y'' o\`u X est le
nombre de variables, c'est \`a dire le nombre de sommets du Graphe, et Y
est le nombre de clauses, c'est \`a dire le nombre de paires dans le
probl\`eme SAT.

Pour la lecture de la solution, on lit la première ligne qui renseigne
la solvabilit\'e du probl\`eme puis on enregistre chaque nombre de la ligne
suivante dans un tableau d'entiers.
Les nombres positifs sont ceux qui appartiennent \`a la couverture mais
le traitement de s\'eparation sera effectu\'e lors de l'\'etape de conversion
de la solution en couverture.

\section{Algorithme de transformation de la solution de minisat en couverture
 de l'instance de VC}
\subsection{Algorithme}
Soit S la solution fournie par minisat sous la forme d'une liste d'entiers.\\
C'est une liste donc $C\gets(v,u)$ signifie que l'on ajoute le couple (a,b) \`a C.

\begin{algorithmic}
\FORALL{$s \in S$}
\IF{$s > 0$}
\STATE $C \gets s$
\ENDIF
\ENDFOR
\end{algorithmic}
\subsection{Commentaires}
A la fin de l'ex\'ecution de l'algorithme, C contient la liste des sommets
de la couverture. La complexit\'e est O(m) o\`u m = |E|.